[−][src]Crate pocket_prover
pocket_prover
A fast, brute force, automatic theorem prover for first order logic
- For generic automated theorem proving, see monotonic_solver
- For a debuggable SAT solver, see debug_sat
extern crate pocket_prover; use pocket_prover::*; fn main() { println!("Socrates is mortal: {}", prove!(&mut |man, mortal, socrates| { // Using `imply` because we want to prove an inference rule. imply( // Premises. and( // All men are mortal. imply(man, mortal), // Socrates is a man. imply(socrates, man), ), // Conclusion. imply(socrates, mortal) ) })); }
Motivation
The motivation is to provide the analogue of a "pocket calculator", but for logic, therefore called a "pocket prover".
This library uses an approach that is simple to implement from scratch in a low level language.
This is useful in cases like:
- Study logic without the hurdle of doing manual proofs
- Checking your understanding of logic
- Verify that logicians are wizards and not lizards
- Due to a series of unfortunate events, you got only 24 hours to learn logic and just need the gist of it
- Memorizing source code for situations like The Martian
- A tiny mistake and the whole planet blows up (e.g. final decisions before the AI singularity and you need to press the right buttons)
In addition this library can be used to create extensible logical systems.
For more information, see the Prove
trait.
Implementation
This library uses brute-force to check proofs, instead of relying on axioms of logic.
64bit CPUs are capable of checking logical proofs of 6 arguments (booleans)
in O(1), because proofs can be interpreted as tautologies (true for all input)
and 2^6 = 64
.
This is done by replacing bool
with u64
and organizing inputs
using bit patterns that simulate a truth table of 6 arguments.
To extend to 10 arguments, T
and F
are used to alternate the 4 extra arguments.
To extend to N arguments, recursive calls are used down to less than 10 arguments.
Path Semantical Logic
Notice! Path Semantical Logic is at early stage of research.
This library has experimental support for a subset of Path Semantical Logic. Implementation is based on paper Faster Brute Force Proofs.
Path Semantical Logic separates propositions into levels, such that an equality between two propositions in level N+1, propagates into equality between uniquely associated propositions in level N.
For example, if f
has level 1 and x
has level 0,
then imply(f, x)
associates x
uniquely with f
,
such that the core axiom of Path Semantics
is satisfied.
This library has currently only support for level 1 and 0.
These functions are prefixed with path1_
.
The macros count!
and prove!
with automatically expand
to path1_count!
and path1_prove!
.
Each function takes two arguments, consisting of tuples of propositions, e.g. (f, g), (x, y)
.
Arbitrary number of arguments is supported.
extern crate pocket_prover; use pocket_prover::*; fn main() { println!("=== Path Semantical Logic ==="); println!("The notation `f(x)` means `x` is uniquely associated with `f`."); println!("For more information, see the section 'Path Semantical Logic' in documentation."); println!(""); print!("(f(x), g(y), h(z), f=g ⊻ f=h) => (x=y ∨ x=z): "); println!("{}\n", prove!(&mut |(f, g, h), (x, y, z)| { imply( and!( imply(f, x), imply(g, y), imply(h, z), xor(eq(f, g), eq(f, h)) ), or(eq(x, y), eq(x, z)) ) })); print!("(f(x), g(y), f=g => h, h(z)) => (x=y => z): "); println!("{}\n", prove!(&mut |(f, g, h), (x, y, z)| { imply( and!( imply(f, x), imply(g, y), imply(eq(f, g), h), imply(h, z) ), imply(eq(x, y), z) ) })); }
Macros
and | An AND relation of variable arguments. |
count | Counts the number of solutions of a variable argument boolean function. |
imply | An IMPLY chain of variable arguments. |
or | An OR relation of variable arguments. |
path1_count | Path Semantical Logic: Counts the number of solutions of a variable argument boolean function. |
path1_prove | Path Semantical Logic: Returns |
prove | Returns |
tup_count | Helper macro for counting size of a tuple. |
tup_set | Helper macro for binding to a tuple pattern. |
xor | An XOR relation of variable arguments. |
Constants
F | The False proposition.
Used to alternate higher than 6 arguments, set to |
P0 | 0xaaaa_aaaa_aaaa_aaaa |
P1 | 0xcccc_cccc_cccc_cccc |
P2 | 0xf0f0_f0f0_f0f0_f0f0 |
P3 | 0xff00_ff00_ff00_ff00 |
P4 | 0xffff_0000_ffff_0000 |
P5 | 0xffff_ffff_0000_0000 |
T | The True proposition.
Used to alternate higher than 6 arguments, set to |
Traits
BaseSystem | Implemented by base logical systems. |
Construct | Used to construct logical systems. |
CoreRules | Implemented by logical systems to define core rules. |
Enumerable | Implemented by types to use with |
ExtendRules | Implemented by logical systems to extend existing ones. |
Prove | Implemented by provable systems of logic. |
Functions
all | Enumerates the type, checking that all outputs are true. |
and | Returns |
and3 | An AND relation of 3 argument. |
and4 | An AND relation of 4 arguments. |
and5 | An AND relation of 5 arguments. |
and6 | An AND relation of 6 arguments. |
and7 | An AND relation of 7 arguments. |
and8 | An AND relation of 8 arguments. |
and9 | An AND relation of 9 arguments. |
and10 | An AND relation of 10 arguments. |
andn | An AND relation of variable number of arguments. |
any | Enumerates the type, checking that at least one output is true. |
count1 | Counts the number of solutions of a 1-argument boolean function. |
count2 | Counts the number of solutions of a 2-argument boolean function. |
count3 | Counts the number of solutions of a 3-argument boolean function. |
count4 | Counts the number of solutions of a 4-argument boolean function. |
count5 | Counts the number of solutions of a 5-argument boolean function. |
count6 | Counts the number of solutions of a 6-argument boolean function. |
count7 | Counts the number of solutions of a 7-argument boolean function. |
count8 | Counts the number of solutions of an 8-argument boolean function. |
count9 | Counts the number of solutions of a 9-argument boolean function. |
count10 | Counts the number of solutions of a 10-argument boolean function. |
countn | Counts the number of solutions of an n-argument boolean function. |
eq | Returns |
false_1 | Ignores argument, always returning |
false_2 | Ignores both arguments, returning |
false_3 | Ignores all 3 arguments, returning |
false_4 | Ignores all 4 arguments, returning |
false_5 | Ignores all 5 arguments, returning |
false_6 | Ignores all 6 arguments, returning |
false_7 | Ignores all 7 arguments, returning |
false_8 | Ignores all 8 arguments, returning |
false_9 | Ignores all 9 arguments, returning |
false_10 | Ignores all 10 arguments, returning |
id | Returns argument. |
imply | First argument implies the second. |
imply3 | An IMPLY chain of 3 arguments. |
imply4 | An IMPLY chain of 4 arguments. |
imply5 | An IMPLY chain of 5 arguments. |
imply6 | An IMPLY chain of 6 arguments. |
imply7 | An IMPLY chain of 7 arguments. |
imply8 | An IMPLY chain of 8 arguments. |
imply9 | An IMPLY chain of 9 arguments. |
imply10 | An IMPLY chain of 10 arguments. |
implyn | An IMPLY chain of variable number of arguments. |
not | If input is |
or | Returns |
or3 | An OR relation of 3 arguments. |
or4 | An OR relation of 4 arguments. |
or5 | An OR relation of 5 arguments. |
or6 | An OR relation of 6 arguments. |
or7 | An OR relation of 7 arguments. |
or8 | An OR relation of 8 arguments. |
or9 | An OR relation of 9 arguments. |
or10 | An OR relation of 10 arguments. |
orn | An OR relation of variable number of arguments. |
path1_count1 | Path Semantical Logic: Counts the number of solutions of a 1-argument boolean function, |
path1_count2 | Path Semantical Logic: Counts the number of solutions of a 2-argument boolean function, |
path1_count3 | Path Semantical Logic: Counts the number of solutions of a 3-argument boolean function, |
path1_count4 | Path Semantical Logic: Counts the number of solutions of a 4-argument boolean function, |
path1_count5 | Path Semantical Logic: Counts the number of solutions of a 5-argument boolean function, |
path1_count6 | Path Semantical Logic: Counts the number of solutions of a 6-argument boolean function, |
path1_count7 | Path Semantical Logic: Counts the number of solutions of a 7-argument boolean function, |
path1_count8 | Path Semantical Logic: Counts the number of solutions of a 8-argument boolean function, |
path1_count9 | Path Semantical Logic: Counts the number of solutions of a 9-argument boolean function, |
path1_count10 | Path Semantical Logic: Counts the number of solutions of a 10-argument boolean function, |
path1_countn | Path Semantical Logic: Counts the number of solutions of a n-argument boolean function, |
path1_countnm | Path Semantical Logic: Counts the number of solutions of a n+m-argument boolean function, |
path1_lennm | Path Semantical Logic: Computes number of cases. |
path1_prove1 | Path Semantical Logic: Returns |
path1_prove2 | Path Semantical Logic: Returns |
path1_prove3 | Path Semantical Logic: Returns |
path1_prove4 | Path Semantical Logic: Returns |
path1_prove5 | Path Semantical Logic: Returns |
path1_prove6 | Path Semantical Logic: Returns |
path1_prove7 | Path Semantical Logic: Returns |
path1_prove8 | Path Semantical Logic: Returns |
path1_prove9 | Path Semantical Logic: Returns |
path1_prove10 | Path Semantical Logic: Returns |
path1_proven | Path Semantical Logic: Returns |
path1_provenm | Path Semantical Logic: Returns |
prop | Returns |
prove1 | Returns |
prove2 | Returns |
prove3 | Returns |
prove4 | Returns |
prove5 | Returns |
prove6 | Returns |
prove7 | Returns |
prove8 | Returns |
prove9 | Returns |
prove10 | Returns |
proven | Returns |
true_1 | Ignores argument, always returning |
true_2 | Ignores both arguments, returning |
true_3 | Ignores all 3 arguments, returning |
true_4 | Ignores all 4 arguments, returning |
true_5 | Ignores all 5 arguments, returning |
true_6 | Ignores all 6 arguments, returning |
true_7 | Ignores all 7 arguments, returning |
true_8 | Ignores all 8 arguments, returning |
true_9 | Ignores all 9 arguments, returning |
true_10 | Ignores all 10 arguments, returning |
xor | Returns |
xor3 | An XOR relation of 3 arguments. |
xor4 | An XOR relation of 4 arguments. |
xor5 | An XOR relation of 5 arguments. |
xor6 | An XOR relation of 6 arguments. |
xor7 | An XOR relation of 7 arguments. |
xor8 | An XOR relation of 8 arguments. |
xor9 | An XOR relation of 9 arguments. |
xor10 | An XOR relation of 10 arguments. |
xorn | An XOR relation of variable number of arguments. |
Type Definitions
Pred1 | A boolean function of one argument. |
Pred2 | A boolean function (transformed) of two arguments. |